'''
Created on 26/06/2009

@author: hurtado
'''
from logica.proposiciones import *
from copy import copy
from settings import SETTINGS

REPR = SETTINGS['palabras_reservadas']

class ReglaInferencia(object):
    pass


# Reglas de inferencia
class ModusPonens(ReglaInferencia):
    def es_aplicable(self, implicacion, antecedente):
        if isinstance(implicacion, Implicacion):
            return implicacion.proposicion1 == antecedente
        return False
    
    def aplicar(self, implicacion, antecedente):
        if self.es_aplicable(implicacion, antecedente):
            return [implicacion.proposicion2,]
        return []
    
    def __repr__(self):
        return REPR['mp']


class ModusTollens(ReglaInferencia):
    def es_aplicable(self, implicacion, neg_consecuente):
        if isinstance(implicacion, Implicacion):
            return (Negacion(implicacion.proposicion2) == neg_consecuente or
                    implicacion.proposicion2 == Negacion(neg_consecuente))
        return False
    
    def aplicar(self, implicacion, consecuente):
        if self.es_aplicable(implicacion, consecuente):
            return [Negacion(implicacion.proposicion1),]
        return []
    
    def __repr__(self):
        return REPR['mt']


class ModusTollendoPonens(ReglaInferencia):
    def es_aplicable(self, disyuncion, neg_proposicion):
        if isinstance(disyuncion, Disyuncion):
            return ((Negacion(disyuncion.proposicion1) == neg_proposicion or
                    disyuncion.proposicion1 == Negacion(neg_proposicion)) or
                    (Negacion(disyuncion.proposicion2) == neg_proposicion or
                    disyuncion.proposicion2 == Negacion(neg_proposicion)))
        return False
    
    def aplicar(self, disyuncion, neg_proposicion):
        p_resultantes = []
        if isinstance(disyuncion, Disyuncion):
            if (Negacion(disyuncion.proposicion1) == neg_proposicion or
                disyuncion.proposicion1 == Negacion(neg_proposicion)):
                p_resultantes.append(disyuncion.proposicion2)
            if (Negacion(disyuncion.proposicion2) == neg_proposicion or
                    disyuncion.proposicion2 == Negacion(neg_proposicion)):
                p_resultantes.append(disyuncion.proposicion1)
        return p_resultantes
    
    def __repr__(self):
        return REPR['mtp']


class Simplificacion(ReglaInferencia):
    def es_aplicable(self, proposicion):
        return isinstance(proposicion, Conjuncion)
    
    def aplicar(self, proposicion):
        p_resultantes = []
        if isinstance(proposicion, Conjuncion):
            p_resultantes.append(proposicion.proposicion1)
            p_resultantes.append(proposicion.proposicion2)
        return p_resultantes
    
    def __repr__(self):
        return REPR['simpl']


class Adjuncion(ReglaInferencia):
    def es_aplicable(self, proposicion1, proposicion2):
        return True
    
    def aplicar(self, proposicion1, proposicion2):
        return [Conjuncion(proposicion1, proposicion2),]
    
    def __repr__(self):
        return REPR['adj']


class SilogismoHipotetico(ReglaInferencia):
    def es_aplicable(self, implicacion1, implicacion2):
        return (isinstance(implicacion1, Implicacion) and 
            isinstance(implicacion2, Implicacion) and
            implicacion1.proposicion2 == implicacion2.proposicion1)
    
    def aplicar(self, implicacion1, implicacion2):
        if self.es_aplicable(implicacion1, implicacion2):
            return [Implicacion(implicacion1.proposicion1, 
                                implicacion2.proposicion2),]
        return []
    
    def __repr__(self):
        return REPR['sh']


class Adicion(ReglaInferencia):
    def es_aplicable(self, proposicion):
        return True
    
    def aplicar(self, proposicion):
        #TODO: pensar en una posible solucion
        return []
    
    def __repr__(self):
        return REPR['adc']


class SilogismoDisyuntivo(ReglaInferencia):
    def es_aplicable(self, disyuncion, implicacion1, implicacion2):
        return (isinstance(disyuncion, Disyuncion) and
                isinstance(implicacion1, Implicacion) and
                isinstance(implicacion2, Implicacion) and
                ((disyuncion.proposicion1 == implicacion1.proposicion1 and
                  disyuncion.proposicion2 == implicacion2.proposicion1) or
                 (disyuncion.proposicion1 == implicacion2.proposicion1 and
                  disyuncion.proposicion2 == implicacion1.proposicion1)))
        
    def aplicar(self, disyuncion, implicacion1, implicacion2):
        if self.es_aplicable(disyuncion, implicacion1, implicacion2):
            return [Conjuncion(implicacion1.proposicion2, 
                               implicacion2.proposicion2),]
    
    def __repr__(self):
        return REPR['sd']


class ReglaPremisas(ReglaInferencia):
    def __repr__(self):
        return REPR['rp']


class Demostrostrado(ReglaInferencia):
    def __repr__(self):
        return REPR['dem']


class PorDemostrar(ReglaInferencia):
    def __repr__(self):
        return REPR['pdem']


class DemostracionCondicional(ReglaInferencia):
    def __repr__(self):
        return REPR['dcond']


class ReduccionAlAbsurdo(ReglaInferencia):
    def __repr__(self):
        return REPR['raa']


class Contradiccion(ReglaInferencia):
    def __repr__(self):
        return REPR['contr']
        

class EspecificacionUniversal(ReglaInferencia):
    def __init__(self, variable=None, objeto=None):
        self.variable = variable
        self.objeto = objeto

    def es_aplicable(self, proposicion, variable):
        if isinstance(proposicion, ProposicionPredicativa):
            return isinstance(proposicion.elementos[variable], Cuantificador)
        return False
        
    def aplicar(self, proposicion, variable, objeto):
        if self.es_aplicable(proposicion, variable):
            p_resultante = copy()
            return []
    
    def __repr__(self):
        return REPR['eu']
        

class GeneralizacionUniversal(ReglaInferencia):
    def __init__(self, objeto=None, variable=None):
        self.variable = variable
        self.objeto = objeto
    
    def __repr__(self):
        return REPR['gu']


class EspecificacionExistencial(ReglaInferencia):
    def __init__(self, variable=None, objeto=None):
        self.variable = variable
        self.objeto = objeto
    
    def __repr__(self):
        return REPR['ee']


class GeneralizacionExistencial(ReglaInferencia):
    def __init__(self, objeto=None, variable=None):
        self.variable = variable
        self.objeto = objeto
    
    def __repr__(self):
        return REPR['ge']


class LeySubalternacion(ReglaInferencia):
    def __repr__(self):
        return REPR['lsa']


class Identidad(ReglaInferencia):
    def __repr__(self):
        return REPR['ident']


class EquivalenciaLogica(ReglaInferencia):
    pass

 
# Equivalencias logicas
class Idempotencia(EquivalenciaLogica):
    def es_aplicable(self, proposicion):
        aplicable = False
        if (isinstance(proposicion, Disyuncion) or
            isinstance(proposicion, Conjuncion)):
            aplicable = proposicion.proposicion1 == proposicion.proposicion2
        elif isinstance(proposicion, ProposicionMolecular):
            aplicable = self.es_aplicable(proposicion.proposicion1)
            if not aplicable and not isinstance(proposicion, Negacion):
                aplicable = self.es_aplicable(proposicion.proposicion2)
        return aplicable
    
    def aplicar(self, proposicion):
        p_resultantes = []
        if isinstance(proposicion, ProposicionMolecular):
            p1_resultantes = self.aplicar(proposicion.proposicion1)
            if not isinstance(proposicion, Negacion):
                p2_resultantes = self.aplicar(proposicion.proposicion2)
            TipoProposicion = proposicion.__class__
            p_resultante = None
            if (isinstance(proposicion, Disyuncion) or
                isinstance(proposicion, Conjuncion)):
                p_resultante = proposicion.proposicion1
                p_resultantes.append(p_resultante)
            for p1_resultante in p1_resultantes:
                p_resultante1 = copy(proposicion)
                p_resultante1.proposicion1 = p1_resultante
                p_resultantes.append(p_resultante1)
            for p2_resultante in p2_resultantes:
                p_resultante1 = copy(proposicion)
                p_resultante1.proposicion2 = p2_resultante
                p_resultantes.append(p_resultante1)
        return p_resultantes
    
    def __repr__(self):
        return REPR['idemp']
    

class Conmutatividad(EquivalenciaLogica):
    def es_aplicable(self, proposicion):
        aplicable = False
        if (isinstance(proposicion, Disyuncion) or
            isinstance(proposicion, Conjuncion) or
            isinstance(proposicion, DobleImplicacion)):
            aplicable = True
        elif isinstance(proposicion, ProposicionMolecular):
            aplicable = self.es_aplicable(proposicion.proposicion1)
            if not aplicable and not isinstance(proposicion, Negacion):
                aplicable = self.es_aplicable(proposicion.proposicion2)
        return aplicable
    
    def aplicar(self, proposicion):
        p_resultantes = []
        if isinstance(proposicion, ProposicionMolecular):
            p1_resultantes = self.aplicar(proposicion.proposicion1)
            if not isinstance(proposicion, Negacion):
                p2_resultantes = self.aplicar(proposicion.proposicion2)
            TipoProposicion = proposicion.__class__
            p_resultante = None
            if (isinstance(proposicion, Disyuncion) or
                isinstance(proposicion, Conjuncion) or
                isinstance(proposicion, DobleImplicacion)):
                p_resultante = TipoProposicion(proposicion.proposicion2,
                                               proposicion.proposicion1)
                p_resultantes.append(p_resultante)
            for p1_resultante in p1_resultantes:
                p_resultante1 = copy(proposicion)
                p_resultante1.proposicion1 = p1_resultante
                p_resultantes.append(p_resultante1)
            for p2_resultante in p2_resultantes:
                p_resultante1 = copy(proposicion)
                p_resultante1.proposicion2 = p2_resultante
                p_resultantes.append(p_resultante1)
        return p_resultantes
    
    def __repr__(self):
        return REPR['conm']


class Asociatividad(EquivalenciaLogica):
    def es_aplicable(self, proposicion):
        aplicable = False
        if ((isinstance(proposicion, Disyuncion) or
            isinstance(proposicion, Conjuncion)) and
            (isinstance(proposicion.proposicion1, proposicion.__class__) or
             isinstance(proposicion.proposicion2, proposicion.__class__))):
            aplicable = True
        elif isinstance(proposicion, ProposicionMolecular):
            aplicable = self.es_aplicable(proposicion.proposicion1)
            if not aplicable and not isinstance(proposicion, Negacion):
                aplicable = self.es_aplicable(proposicion.proposicion2)
        return aplicable
    
    def aplicar(self, proposicion):
        p_resultantes = []
        if isinstance(proposicion, ProposicionMolecular):
            p1_resultantes = self.aplicar(proposicion.proposicion1)
            if not isinstance(proposicion, Negacion):
                p2_resultantes = self.aplicar(proposicion.proposicion2)
            TipoProposicion = proposicion.__class__
            p_resultante = None
            if (isinstance(proposicion, Disyuncion) or
                isinstance(proposicion, Conjuncion)):
                if isinstance(proposicion.proposicion1, TipoProposicion):
                    proposicion1 = proposicion.proposicion1
                    p2_resultante = TipoProposicion(proposicion1.proposicion2,
                                                    proposicion.proposicion2)
                    p_resultante = TipoProposicion(proposicion1.proposicion1,
                                                   p2_resultante)
                    p_resultantes.append(p_resultante)
                if isinstance(proposicion.proposicion2, TipoProposicion):
                    proposicion2 = proposicion.proposicion2
                    p1_resultante = TipoProposicion(proposicion.proposicion1,
                                                    proposicion2.proposicion1)
                    p_resultante = TipoProposicion(p1_resultante,
                                                   proposicion2.proposicion2)
                    p_resultantes.append(p_resultante)
            for p1_resultante in p1_resultantes:
                p_resultante1 = copy(proposicion)
                p_resultante1.proposicion1 = p1_resultante
                p_resultantes.append(p_resultante1)
            for p2_resultante in p2_resultantes:
                p_resultante1 = copy(proposicion)
                p_resultante1.proposicion2 = p2_resultante
                p_resultantes.append(p_resultante1)
        return p_resultantes
    
    def __repr__(self):
        return REPR['asoc']
    
    
class Distributividad(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['dist']


class DefinicionImplicacion(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['impl']


class DefinicionDobleImplicacion(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['dimpl']


class LeyDeMorgan(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['ldm']


class ElementoNeutro(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['eneutro']


class CondicionTautologia(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['taut']


class CondicionAntitautologia(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['ataut']


class Absorcion(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['abs']


class DobleNegacion(EquivalenciaLogica):
    
    def __repr__(self):
        return REPR['dneg']


class IntercambioCuantificadores(ReglaInferencia):
    
    def __repr__(self):
        return REPR['intcuant']


class DistributividadCuantificadores(ReglaInferencia):
    
    def __repr__(self):
        return REPR['distcuant']
